T:Type, P:(L:(T List)(||L||-1)||L||), L:T List. count(i<j<||L|| : P L i j)   

latex

Definitions	t  T, , x:A. B(x), {i..j}, ||as||, count(i<j<||L|| : P L i j), ij, P  Q, False, A, P & Q, AB, i  j < k, i<j, p  q, if b t else f fi, , x,y. t(x;y), Prop, True, b, b, ij, T, P  Q, P  Q, Unit, sum(f(x) | x < k), x. t(x), sum(f(x;y) | x < n; y < m)
Lemmas	assert of bnot, not wf, non neg sum, sum wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, le int wf, assert wf, bnot wf, le wf, double sum wf, non neg length, ifthenelse wf, band wf, lt int wf, length wf1, int seg wf, bool wf